(set-logic QF_NIA)
(declare-fun i13 () Int)
(declare-fun i17 () Int)
(declare-fun i18 () Int)
(declare-fun v57 () Bool)
(assert (or v57 (= i18 i17)))
(assert (> 0 i17))
(assert (= (* i13 (- i13 1)) (* i17 (- i17))))
(check-sat)
